/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package logical;

import java.util.ArrayList;
import java.util.List;
import tool.StringTool;

/**
 *
 * @author julien
 */
public class Formula extends LogicalElement {

    private List<Connector> connectors = new ArrayList<Connector>();
    private List<LogicalElement> formulaElements = new ArrayList<LogicalElement>();
    private Formula CNFEquivalentFormula;

    //Constructeur basique
    public Formula(List<LogicalElement> formulaElements, List<Connector> connectors) {
        this.connectors = connectors;
        this.formulaElements = formulaElements;
        this.CNFEquivalentFormula = getConvertedFormulaToCNFForm();
    }

    //Constructeur à partie d'une formule latex
    public Formula(String latexFormula) {
        //Enlever les parenthèses et les espaces de début et de fin si elles existent
        String formulaToParse = StringTool.removeFirstAndLastParenthesis(latexFormula);
        formulaToParse = formulaToParse.toLowerCase();
        System.out.println(formulaToParse);

        //Recherche le prochain mot 
        String nextStringToAnalize = "";
        Boolean notEnable = false;
        while (!formulaToParse.equals("")) {
            // On prend le premier élément de la formule
            formulaToParse = formulaToParse.trim();
            String[] temp = formulaToParse.split(" ", 2);
            nextStringToAnalize = temp[0];
            if (temp.length > 1) {
                formulaToParse = temp[1];
            } else {
                formulaToParse = "";
            }
            //Une parenthèse ouvrante signifie une nouvelle formule
            //On parse tout ce qui se trouve jusuqu'a la parenthèse fermante en tant que nouvelle formule
            //On verifie qu'il y ait au moins un connecteur dans cette parenthèse sinon ce n'est pas une formule
            if (nextStringToAnalize.equals("(")) {
                int indexOfClosedParenthesis = StringTool.findIndexOfClosedParenthesis(formulaToParse);
                String formulaInParenthesis = formulaToParse.substring(0, indexOfClosedParenthesis);
                formulaToParse = formulaToParse.substring(indexOfClosedParenthesis + 1, formulaToParse.length());
                System.out.println("Open Parenthesis found, parse " + formulaInParenthesis);
                formulaElements.add(new Formula(formulaInParenthesis, notEnable));
                notEnable = false;
            } else {
                //AND, OR, IMPLY,EQUIV identifé comme un connecteur
                if (nextStringToAnalize.equals(
                        "and")) {
                    connectors.add(Connector.AND);
                    System.out.println("AND found");
                } else {
                    if (nextStringToAnalize.equals("or")) {
                        connectors.add(Connector.OR);
                        System.out.println("OR found");
                    } else {
                        if (nextStringToAnalize.equals("imply")) {
                            connectors.add(Connector.IMPLY);
                            System.out.println("IMPLY found");
                        } else {

                            if (nextStringToAnalize.equals("equiv")) {
                                connectors.add(Connector.EQUIV);
                                System.out.println("EQuIV found");
                            } else {
                                if (nextStringToAnalize.equals("not")) {
                                    //un NOT dans ce cas on le garde en mémoire et on continu l'analyse
                                    System.out.println("NOT Found");
                                    notEnable = !notEnable;
                                } else {
                                    //Mot quelconque, identifié comme un atome
                                    formulaElements.add(new Atom(nextStringToAnalize, nextStringToAnalize, notEnable));
                                    notEnable = false;
                                    System.out.println("Atom found : " + nextStringToAnalize);
                                }
                            }
                        }
                    }
                }

            }
        }
        this.CNFEquivalentFormula = getConvertedFormulaToCNFForm();
    }

    //Constructeur à partir d'une formule avec possibililité de NOT
    public Formula(String latexFormula, Boolean negate) {
        this(latexFormula);
        this.negate = negate;

    }

    public List<Connector> getConnectors() {
        return connectors;
    }

    public List<LogicalElement> getFormulaElements() {
        return formulaElements;
    }

    @Override
    public String getLiteralTranslation() {
        /* Vérification de la validité d'une formule
        if (connectors.size() != formulaElements.size() -1) {
        throw new BadFormulaException("Number of Connectors does not match");
        } */
        int index = 0;
        String translation = "(" + formulaElements.get(index).getLiteralTranslation();
        while (index < formulaElements.size() - 1) {
            translation += " " + connectors.get(index);
            index++;
            translation += " " + formulaElements.get(index).getLiteralTranslation();
        }
        return translation + ")";
    }

    @Override
    public String getLatexTranslation() {
        int index = 0;
        String translation = "(" + formulaElements.get(index).getLatexTranslation();
        while (index < formulaElements.size() - 1) {
            translation += " " + connectors.get(index);
            index++;
            translation += " " + formulaElements.get(index).getLatexTranslation();
        }
        return translation + ")";
    }

    @Override
    public String getSATTranslation() {
        // Dans la formule CNF tous les éléments logiques sont des atomes 
        // et tous les connecteurs sont des AND ou des OU
        for (Connector c : CNFEquivalentFormula.getConnectors()) {
            if ((c != Connector.AND) && (c != Connector.OR)) {
                return null;
            }
        }
        for (LogicalElement l : CNFEquivalentFormula.getFormulaElements()) {
            if (l instanceof Formula) {
                return null;
            }
        }
        //Début de la traduction
        String translation = formulaElements.get(0).getSATTranslation();
        int index = 0;
        while (index < formulaElements.size() - 1) {
            switch (connectors.get(index)) {
                case AND: {
                    translation += " 0\n";
                    break;
                }
                case OR: {
                    translation += " ";
                    break;
                }
            }
            index++;
            translation += formulaElements.get(index).getSATTranslation();
        }
        translation += " 0";
        return translation;
    }

    @Override
    public Formula getCNFForm() {
        return CNFEquivalentFormula;
    }

    @Override
    public Integer getNumberofAtoms(boolean takeCareAboutDuplicate) {
        //TODO Construire la méthode de comptage des atomes en compte les doublons
        Integer count = 0;
        for (LogicalElement elements : formulaElements) {
            count += elements.getNumberofAtoms(takeCareAboutDuplicate);
        }
        return count;
    }

    // Cette méthode change la formule sous sa forme CNF
    // Elle ne doit être appelée qu'une seule fois lors de l'instanciation de la formule
    private Formula getConvertedFormulaToCNFForm() {
        Formula formulaToReturn = this ;
        //Remplacement des EQUIV par double implication
        //A EQUIV B se réécrit (A IMPLY B) et (B IMPLY A)
        //Ou encore (NOT A OR B) AND (Not B OR A)
        LogicalElement A;
        LogicalElement B;
        //Construction du connecteur OR
        List<Connector> orConnector = new ArrayList<Connector>();
        orConnector.add(Connector.OR);
        //Constructeur de la liste des éléments logiques
        List<LogicalElement> newElements = new ArrayList<LogicalElement>();
        //Parcours de la formule
        int index = 0;
        while (index < connectors.size()) {
            if (connectors.get(index) == Connector.EQUIV) {
                connectors.set(index, Connector.AND);
                A = formulaElements.get(index);
                B = formulaElements.get(index + 1);
                A.negateElement();
                newElements.add(A.getCNFForm());
                newElements.add(B.getCNFForm());
                formulaElements.set(index, new Formula(newElements, orConnector));
                newElements.clear();
                B.negateElement();
                A.negateElement();
                newElements.add(A.getCNFForm());
                newElements.add(B.getCNFForm());
                formulaElements.set(index + 1, new Formula(newElements, orConnector));
                
            }
            index ++ ;
            System.out.println("Conversion test :" +formulaToReturn.getLatexTranslation());
        }

        //Remplacement des IMPLY
        index = 0;
        while (index < connectors.size()) {
            if (connectors.get(index) == Connector.IMPLY) {
            }
            index ++ ;
        }
        //Déplacement des NOT à l'intérieur des formules

        //Distribution des OR ou des ET en utilisant les lois de Morgan
        
        return formulaToReturn ;

    }

    public static void main(String[] args) {
        Formula f = new Formula("A and (B or C) or (not b and d) and not e");
        System.out.println(f.getLiteralTranslation());
        System.out.println(f.getLatexTranslation());
        System.out.println(f.getNumberofAtoms(true));
        System.out.println(f.getSATTranslation());
        Formula f2 = new Formula("A EQUIV B");
    }
}
